A:Type, I:MaInterface(A), i:Id.
(i  ma-interface-locs(I))
 (ma-interface-conds(I;i)
 (=
 ((I(i).2)
 ( k:Knd fp V:Type  (State(ma-interface-ds(I;i))V(A + Top))) 

latex

Definitions

MaInterface(T), ma-interface-locs(I), ma-interface-conds(I;i), a:A fp B(a), State(ds), ma-interface-dom(I;i), ma-interface-valtype(I;i;k), fpf-domain(f), ma-interface-ds(I;i), f(x)?z, ma-interface-code(I;i;k), ma-interface-info(I;i;k), f(x), x  dom(f), x:A. B(x), <a, b>, , A c B, l[i], , , A  B, False, ||as||, t.1, x. t(x), x.A(x), Knd, f(a), t.2, if b then t else f fi , Top, left + right, Unit, P  Q, P & Q, , A, x:A. B(x), P  Q, x:AB(x), {x:A| B(x)} , b, x:A  B(x), (x  l), a < b, Id, Atom$n, s = t, type List, Type, t  T, hasloc(k;i), Void, #$n, deq-member(eq;x;L), IdDeq, b, S  T, IdLnk, let x,y = A in B(x;y), True, case b of inl(x) => s(x) | inr(y) => t(y), ff, tt, suptype(S; T), Dec(P)

Lemmas

l member in subtype2, decidable assert, l member type, subtype-set-hasloc, subtype rel set, subtype rel function, btrue wf, bfalse wf, l member subtype, false wf, true wf, IdLnk wf, bool wf, assert wf, not wf, bnot wf, top wf, pi2 wf, id-deq wf, deq-member wf, hasloc wf, Knd wf, assert-deq-member, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, ifthenelse wf, pi1 wf, l member wf, select wf, length wf1